Inference at * 
Iof proof for Lemma comp id r:


  A, B:Type, f:(AB). (f o Id{A}) = f 

latex

 by Unfold `tidentity` 0 

latex

 1: 

 1:   A, B:Type, f:(AB). (f o Id) = f
 .

Definitions

Id{T}